Inference at * 1 
Iof proof for Lemma p-fun-exp-compose:



1. T : Type
  h, f:(T(T + Top)). p-id() o h   = h 

latex

 by (Auto) 
CollapseTHEN ((BLemma `p-id-compose`) 
CollapseTHEN (Auto)) 

latex

C.

Definitions	s = t, x:AB(x), left + right, Top, x:A. B(x), t  T
Lemmas	p-id-compose